$\forall$${\it es}$:ES, $i$, $x$:Id, $T$:Type, $P$:($T$$\rightarrow$Prop), ${\it Lx}$:Knd List.
\\[0ex]es{-}frame(${\it es}$;$i$;${\it Lx}$;$x$;$T$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. (kind($e$) $\in$ ${\it Lx}$) $\Rightarrow$ $P$($x$ when $e$) $\Rightarrow$ $P$(($x$ after $e$))
\\[0ex]$\Rightarrow$ @$i$ stable ${\it state}$.$P$(${\it state}$.$x$)